Repository navigation
Conversation
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nt and one Bool value type An application of a derived Arrow now takes the type the Arrow declares it returns (read from the return atom as written), and a bodied Arrow is admitted only when its body's type equals that return, else arrow_body_does_not_inhabit_declared_return. Before this, no application derived, Int included, and eval refused both Int and Bool applications. dag_binding_denotation is the one binding->value-type join, and its rows point at v2.std.integer integer_int_type_node and v2.std.logic bool_node. The literal rules consume it, a type-name atom derives its kind (TypeDenotationKind), and the evaluator's own Int and Bool type nodes are replaced by the same authorities. Model and ruling are in docs/plans/arrow-elimination-model.md; the composed-evidence defect is filed as function_type_evidence_carries_its_body. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… kind, not the retired inhabitant denotation The parameter conj's composed evidence carries each Int type atom's derived grounding. After the arrow-elimination ruling that grounding is the atom's kind (TypeDenotationKind); the control still asserted the roster's Int inhabitant record, the denotation this PR retired. Found by the srv1 base-vs-head run over the v2 infer/eval/compile test modules (the one true->false). The partial-evidence control's use of the inhabitant node as a roster member is unrelated and unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_discharge to holds/violated; one runtime encoding of true - infer_arrow_elimination eval control: after the merge of main (#12375) infer returns ObligatedInferredTree, so the control reaches eval through discharge_refinement_obligations, the only route to an InferredTree. - refinement_discharge's frontier row flips as it said it would: a true predicate admits, a false one refuses refinement_predicate_violated. The undischargeable arm is kept over a genuinely unevaluable application (an undenoted return). - The flip exposed two runtime encodings of true: v2_eval_bool_true_primitive was a one-bit byte while every evaluated Bool is built by v2_eval_bool_runtime_value (eight bits), so discharge read an evaluated true as violated. The primitive is now that constructor's value. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…; cut every consumer root-first Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…heck clean) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…over-reached) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…parameter_order, reference_closure) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… conflict with #12361) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
THE GAP. v2.compiler.infer's infer_node_facts routes a declaration reference --
Conj-shaped, so infer_atom_binding_sym answers Absent -- straight to
inferred_facts_not_derived. An entry IS admitted for the node and its grounding is
GroundingNotDerived, so inference ACCEPTS the tree and eval refuses later at
whatever consumes it. Nothing typed a reference to a function.
THE REPAIR, IN ONE ARM. Resolution answers WHICH declaration a reference denotes
and carries it as a declaring path; this arm answers WHAT TYPE that declaration
establishes for the use. Two questions, two stages: nothing here re-resolves a
name and resolution mints no types.
declaration_reference_path_optional(n) the declaring path, never the leaf
symbol_index_lookup(resolved.symbol_index, path) the GUARDED read: a path with
more than one bound declaring
answers Absent, so a contested
binding cannot yield a type
arrow_domain_binder_labels(declared.children) evidence check
inferred_facts_from_derived_type(n, declared) evidence attached to the USE
A LOOKUP HIT IS NOT TYPE EVIDENCE. The index is built from validated normalized
roots, which does not establish that every indexed declaration carries usable type
evidence, so this arm does not ground on presence. A callable's evidence is its
Arrow and the check is that its domain reads; an unsupported or unresolved
signature stays explicitly ungrounded. Non-callable declarations are left to their
own derivation rather than stamped.
THE EVIDENCE ATTACHES TO THE USE. derived_type is the DECLARATION's node while the
entry is keyed by the REFERENCE node, so the use keeps its own occurrence and
locus and canonical_grounding_from_derived_type's self-evidence refusal still
holds.
THE CARRIER IS #12432's, CONSUMED NOT REBUILT. ResolvedTree { root, symbol_index }
already reaches fn infer(tree: ResolvedTree); it was never threaded past there --
symbol_index appeared exactly once in 04_infer.dag, in a comment. The thread is
`resolved: ResolvedTree` under a NEW name at every site, not a second
`index: SymbolIndex` parameter: passing root and index side by side lets them come
from different trees and disagree, and nothing would stop it, while the paired
carrier makes the mismatch unwritable (DESIGN section 5, construction over
validation). Functions that want the root read resolved.root.
ELEVEN FUNCTIONS, NOT THE SIX ESTIMATED. The compiler found the other five --
infer_gather_transform_row_on_entries, infer_gather_application_row_on_entries,
infer_gather_bind_annotation_row_on_entries, infer_gather_fold_step_merged,
infer_gather_settled_row -- which is the argument for renaming at every site
rather than adding a parallel parameter. Non-path callees keep `tree: Node` and
receive resolved.root, so their contracts are untouched. The thread landed first
as a 41/41 behaviour-neutral change, verified by the regression guards passing
with the control still red, so any guard breakage would be attributable to the
derivation rather than the rename.
PARAMETER TYPING IS NOT REPLACED. infer_parameter_scope_search /
infer_parameter_type_in_scope stay. Their comment names "the SymbolIndex /
ResolvedTree.bindings lookup" as their dissolution trigger, and it is tempting to
read this change as that trigger; it is not. A local use resolves to a canonical
Atom at its own occurrence and never acquires a declaring path, so the index
answers a different question. What was established here is only that
symbol_index_fill puts Arrow DOMAINS in the index -- a fact about fill, not about
what a parameter use resolves to. Deleting the walk on that basis would have
reintroduced the defect its comment records: `fn positive(x: Int)` beside
`fn f(x: Pos)` grounding every `x` in `f` as Int.
EVIDENCE.
dre_a_reference_grounds_to_its_declarations_contract_holds FAIL -> PASS
bcn_cast_into_a_refinement_refuses_at_infer PASS unchanged
bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS unchanged
bcn_identity_cast_into_a_refinement_admits PASS unchanged
The control asserts the CONTRACT, not the grounding tag: it selects every node
whose decoded declaring path ends in the wanted leaf, requires EXACTLY ONE, and
requires the derived type's Arrow domain to bind exactly the name the fixture
text specifies. A DerivedGrounding carrying the wrong type fails it.
NOT QUALIFIED, STATED AS SUCH. dre_a_same_leaf_reference_gets_its_own_declarations
_contract_holds passes but is NOT yet an identity-collapse detector. The forced-
collapse mutation turned BOTH controls red rather than only the same-leaf one,
because the mutation's path does not exist in the first fixture either -- it broke
everything instead of specifically collapsing identity. Within a single-module
fixture the discriminating case cannot be built: a reference that reaches this arm
denotes a module-level callable whose declaring path IS [module, leaf], so path
and leaf coincide. Qualifying it needs a two-module fixture where each module
declares the same leaf. Until that runs, this control is specified, not qualified.
NOT DONE HERE. The application connection (#12379's rule wants a callee Arrow, and
a reference now grounds to one) and the s3 end-to-end assertion are the next step,
and the outer equality may still lack a typing rule of its own.
Based on #12432 (ResolvedTree carrier) and #12379 (application-result typing);
rebases onto #12379, which lands first.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
MY COMMENT CLAIMED MORE THAN MY GUARD CHECKED. The arm grounded a reference when arrow_domain_binder_labels could read the declaration's parameter names, and the comment beside it said an unsupported or unresolved signature stayed ungrounded. That was false of the guard. That reader takes only `children`, so it never establishes the declaration IS an Arrow, and it inspects no parameter type, no return type, no scope and no body. "I can read the parameter names" is a different property from "this declaration establishes this callable type", and the comment asserted the second while the code checked the first -- rung inflation in the annotation, caught in review rather than by a control, because no control distinguished the two. THE GUARD IS NOW THE APPLICATION PATH'S OWN REQUIREMENTS, reused rather than restated: infer_operator_arrow (the node IS an Arrow), infer_formals_from_domain (every formal is named), and arrow_declared_parameter_order, where both Absent and Malformed refuse -- the domain is sorted by label for identity, so its stored sequence is not the declared order and an Arrow without the order edge is one a binder already refuses. Grounding a reference whose declaration cannot satisfy those would mint evidence no consumer can use. WHAT IT STILL DOES NOT ESTABLISH, stated rather than implied: the type references inside that signature are not resolved in the declaration's scope here, and no body or return obligation is discharged. Those stay with the existing inference contract; a reference consuming a declared signature does not recheck a body at every use. The claim is the structural callable contract and nothing wider. Controls unchanged in outcome and now discriminating for the right reason: dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
FIVE ATTEMPTS, NO DISCRIMINATING CONTROL. A single-module fixture cannot produce one: a reference reaching this arm denotes a module-level callable whose declaring path IS [module, leaf], so path and leaf coincide and a leaf-keyed lookup is accidentally right. A two-module fixture reaches the right shape -- two modules each declaring `shared(alpha: ...)` with different types, the consumer importing one -- but the assertion needs the parameter's declared TYPE read out of the derived Arrow's domain, and neither a walk-order atom search nor find_named_child on the domain produced it. The control stayed GREEN under a mutation that forced the wrong declaration, and then went RED on correct code once the reader changed: both arms wrong, so it distinguished nothing. A green control that does not discriminate is worse than no control, because it would be cited as coverage. A red one blocks the PR while asserting nothing. So neither ships; the gap is recorded where the control would have been. WHAT IS THEREFORE NOT CLAIMED: that this arm resists declaration-identity collapse. The declaring path is what it looks up and symbol_index_lookup is the guarded read, but no executed control here demonstrates that a leaf-keyed answer would be caught. Qualifying it needs a reliable reader for a parameter's declared type inside a derived Arrow domain; that reader is the missing piece. Retained and passing: the two controls that do discriminate their own properties, and the three refinement guards. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…still is not enough THE CONNECTION WAS ABSENT IN CODE, not merely unmeasured. infer_application_callee_arrow read the callee EXPRESSION's own kind through infer_operator_arrow, and a resolved declaration reference stays a Conj however well typed it is -- so the helper answered Absent for it and every consumer (formals, type parameters, argument inhabitance, result typing) fell through to the undecidable-accepted arm. Giving the reference callable facts did not make any of them read those facts. Adding evidence and consuming evidence are two changes and only the first had landed. infer_application_callee_arrow_with_facts falls back to the callee's own facts entry when the node is not itself an Arrow, taking ONLY the type from DerivedGrounding's structural evidence. The use keeps its node and occurrence; the declaration's body and identity are not substituted. Wired at the three sites that asked the old helper, with entries threaded into infer_application_formals and infer_application_type_params -- the other two callers already carried entries. NECESSARY, NOT SUFFICIENT, AND THE CONTROL SAYS SO. A named call still does not ground. dre_a_named_call_is_grounded_expected_red is enrolled as an executed expected-red rather than a passing claim or a deleted one: the boundary is real, its cause is not yet identified, and naming it is the next step rather than widening the reader until something goes green. What is missing between a grounded callee and a grounded application is unestablished -- I did not determine whether the call's facts entry is absent or present-and-ungrounded, and that distinction picks the repair. Guards unchanged, including the two application-typing rows: bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS dre_a_reference_grounds_to_its_declarations_contract_holds PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e type
THE REMAINING FAILURE WAS ONE MISKEYED LOOKUP. After the application path could SEE
a reference's callable evidence, the call still did not ground, and the cause was
in infer_transform_application_optional:
match infer_application_callee_arrow_with_facts(...) {
Present { value: arrow } =>
match lookup_inferred_facts_in_entries(entries: entries, key: arrow) {
That key is right only while an arrow can be the callee node itself. Once the arrow
may be a DECLARATION's Arrow reached through the use's facts, it is a node of the
declaring module with no entry in this tree, so the lookup answered Absent and the
application dropped to the frontier however well the callee was typed. The grounding
question is about the CALLEE USE; the arrow supplies only the TYPE. They are two
things and only the first has facts here. infer_application_callee_use names the
first; the second stays what it was.
dre_a_named_call_is_grounded_holds goes from an enrolled expected-red to a passing
claim on that one change.
A BOOL-RETURNING CALL STILL DOES NOT GROUND, AND IT IS A DIFFERENT BOUNDARY.
Measured three ways on this base: an Int-returning call grounds; a Bool-returning
call with a literal body does not; a Bool-returning call whose body is its own
parameter does not either. The variable is the RETURN TYPE, not the body, and the
reference itself grounds in every one of the three -- so this sits downstream of the
reference repair, in the application's return derivation,
infer_arrow_declared_return_type -> dag_binding_denotation. Enrolled as an executed
expected-red rather than deleted or chased: which binding symbol a Bool return
actually carries is the next question and answering it is a separate change.
THE EXECUTION CONTROL IS DELIBERATELY BOOL-RETURNING, which is why the boundary
surfaced here rather than later: an Int-returning call compared with `==` would have
coupled the first execution proof to equality, which has its own unproven typing.
Guards unchanged, including both application-typing rows:
bcn_cast_into_a_refinement_refuses_at_infer PASS
bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS
bcn_identity_cast_into_a_refinement_admits PASS
bcn_infer_admits_int_to_int PASS
bcn_infer_refuses_int_to_bool PASS
dre_a_reference_grounds_to_its_declarations_contract_holds PASS
dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
INT MASKED THE READER'S ASSUMPTION AND BOOL EXPOSED IT. infer_arrow_declared_return_type sent every return Atom's identity to dag_binding_denotation, which is a BINDING-to-type operation. Int survives that because its canonical type constructor retains the historical spelling ^dag_binding_type_int, so its binding and type identities coincide and a second denotation is a no-op. Bool arrives as the DENOTED node -- v2.std.logic bool_node, ^bool_node_symbol -- so the binding lookup answered Absent and BOTH consumers of this shared reader lost the return: application result typing dropped to the frontier, and the body-versus-declared-return check skipped its comparison. MEASURED BEFORE REPAIRING. An Int-returning call grounds; a Bool-returning call with a literal body does not; a Bool-returning call whose body is its own parameter does not either. The reference itself grounds in all three, so the variable is the RETURN TYPE and not the body. The return atom was then read directly: Int carries ^dag_binding_type_int, Bool carries ^bool_node_symbol. THE REPAIR RECOGNISES BY AUTHORITY, NOT BY SPELLING. The established case is compared against v2.std.logic's own bool_node() through the existing structural equality, rather than teaching a second meaning for ^bool_node_symbol here or widening dag_binding_denotation to accept a denoted symbol -- that lookup stays strictly binding-to-type, so a specimen fix does not become a muddied contract. Ordered denotation-first, so the Int path is byte-identical and only a return the binding lookup cannot denote reaches the established-type question. ONE reader, so introduction and elimination cannot disagree about the same signature. dre_a_named_call_to_a_bool_fn_is_grounded_holds: expected-red -> PASS. THE MISMATCH NEGATIVES ARE RED, AND THAT IS PRE-EXISTING, NOT INTRODUCED. infer ACCEPTS a Bool-declared function with an Int body and the converse. The cause is upstream of this reader: infer_arrow_body_inhabits_declared_return is only reached when the Arrow carries evidence edges; without them the arm answers inferred_facts_not_derived, and a frontier is not a refusal, so the comparison never runs. Verified by reverting ONLY the return reader and re-running -- both rows fail identically. Enrolled as executed expected-reds rather than deleted: they are exactly the controls that would catch a return recognition which admitted nodes without activating the check, they cannot discharge that duty while the check is unreachable, and when the evidence-edge condition is repaired they become its guard without anyone rediscovering the shape. The eight input-inspection diagnostics that located this are removed; their results are recorded above rather than left as permanent obligations. Guards unchanged: bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS dre_a_named_call_is_grounded_holds PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… again THE PREREQUISITE WAS THE RETURN ATOM'S OWN GROUNDING, not the check. infer_arrow_body_inhabits_declared_return runs only when infer_product_child_evidence_edges answers Present, and that collector requires EVERY Arrow child to carry a resolved type. A Bool return atom carried none, so the whole Arrow dropped to inferred_facts_not_derived -- the frontier -- and the comparison never ran. A frontier is not a refusal, which is why a Bool-declared function with an Int body was ACCEPTED rather than reported. So the same defect had two faces: the reader could not denote an already-denoted return (fixed in 53022c2), and infer_node_facts could not ground one either. Both are the same assumption -- that a type-position Atom is a binding awaiting denotation -- and Int masked both because its binding and type identities coincide. THE SECOND HALF, BY THE SAME AUTHORITY. The denotation arm of infer_node_facts now consults infer_established_return_type_optional, which compares against v2.std.logic's own bool_node() through the existing structural equality. One recognition, reused; no second meaning for ^bool_node_symbol, and dag_binding_denotation still stays strictly binding-to-type. Ordered after the binding lookup, so every previously-denoted path is byte-identical. UNAVAILABLE EVIDENCE DID NOT BECOME A PASSED CHECK. The repair makes the return atom GROUND, which makes the check RUN, which makes the mismatch REFUSE. Nothing was forced to ground to get there and no refusal was weakened: the two controls went from ACCEPTED (wrongly) to REFUSED (correctly), which is the opposite direction from admitting more nodes. dre_a_bool_declared_int_body_still_refuses_holds expected-red -> PASS dre_an_int_declared_bool_body_still_refuses_holds expected-red -> PASS Reference typing, application typing and the return derivation stay connected: dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS dre_a_named_call_is_grounded_holds PASS dre_a_named_call_to_a_bool_fn_is_grounded_holds PASS bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…efused FOUR CONTROLS, BATCHED ON THE PINNED BASE. dre_an_unresolved_signature_does_not_ground_holds PASS dre_an_invalid_argument_call_does_not_ground_holds PASS dre_an_imported_reference_grounds_the_same_way_holds PASS (with the two mismatch negatives promoted in 5359640) UNAVAILABLE EVIDENCE DOES NOT BECOME A PASSED CHECK. A signature whose parameter type names nothing reads structurally and means nothing: the shape is readable, the evidence is not, and the reference stays underived. That is the control a permissive fallback would have turned green, and it is the one that keeps infer_declaration_callable_evidence honest about what "callable evidence" claims. AN INVALID ARGUMENT DOES NOT GROUND THE CALL. A Bool passed where the declared parameter is Int leaves the application ungrounded, so the contract is not satisfied merely because the callee's type was found. THE IDENTITY DISCRIMINATOR IS NOW QUALIFIED, and by the mutation that the earlier five attempts could not construct. Those attempts failed because a single-module fixture cannot separate path from leaf -- a module-level callable's declaring path IS [module, leaf]. Across two modules it separates: repointing the imported reference's lookup at a DIFFERENT EXISTING declaration (m.app rather than m.lib.helper, so the lookup still SUCCEEDS) turns that row red while the same-module call stays green. That is wrong-declaration selection being detected, which an absent-path mutation could never establish -- it tests missing evidence instead. So the claim this PR would not make three commits ago is now made on executed evidence: the arm resists declaration-identity collapse. Full set on the pinned base 80e9a04: dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS dre_a_named_call_is_grounded_holds PASS dre_a_named_call_to_a_bool_fn_is_grounded_holds PASS dre_a_bool_declared_int_body_still_refuses_holds PASS dre_an_int_declared_bool_body_still_refuses_holds PASS dre_an_unresolved_signature_does_not_ground_holds PASS dre_an_invalid_argument_call_does_not_ground_holds PASS dre_an_imported_reference_grounds_the_same_way_holds PASS bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
THE TYPING IS DONE; THE EXECUTION IS NOT, AND THE BOUNDARY IS ELSEWHERE.
A named Bool-returning call now grounds under infer -- reference typing, application
typing and the return derivation all reached -- and the same call through the REAL
native route refuses at EVAL with eval_rejected_grounding_not_derived at a SYNTHETIC
node carrying no authored locus.
So this lane's subject is complete in the sense it was scoped: a reference obtains a
justified callable contract, the application consumes it, valid and invalid cases
separate, and the body/return check is reachable again. What it does not deliver is
an executed assertion, because eval's facts gate is asked about a node this lane
never touches.
THE FALSE CONTROL EARNED ITS PLACE BY NOT DISCRIMINATING. Both rows refused
identically, so neither body ran and a refusal is indistinguishable from a false
answer at this point. Had only the positive row existed, the same outcome would have
read as "the call returned false" rather than "nothing executed".
THE SIGNATURE IS NOT NEW, which is the useful part: a plain-binder match over a
coproduct, and a trivial `fn f(b: Box) -> Int { 7 }` whose assertion never touches a
field, both refuse at eval on this same cause at a synthetic node. Three unrelated
subjects, one wall. That says the next boundary is eval's grounding consumer and not
anything about calls, and it is where the next lane should start rather than
rediscovering it.
Enrolled executed as expected-reds rather than deleted, so the measurement survives
in the corpus with its subject attached.
nc_a_named_bool_call_executes_expected_red eval refusal
nc_the_false_returning_call_is_the_deliberate_false_control_expected_red eval refusal
universe=2 population=2 file_refusals=8
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ng path
The native qualification refused with eval_rejected_grounding_not_derived on a
node the renderer prints only as "<synthetic node occurrence>", which is a
PROVENANCE CATEGORY and not an identity -- so that log alone could not say which
node, and could not distinguish this from an unrelated universal eval defect.
This control supplies the same call shape at the eval boundary and reads the
refusal anchor directly. It is the one comparison that decides it, and it says:
the anchor is a node strictly inside the callee reference's encoded declaring
path.
So eval is demanding value-grounding for the internal representation of a
declaration identity rather than consuming that identity as a reference. The
route is established by source and now confirmed by measurement:
eval_node_is_callee_reference admits an Arrow and a bare Atom only
-> a resolved reference is a MARKED CONJ (resolve resolved_reference_node)
-> the callee edge is not recognized, eval_fold_child_for_edge takes its
ordinary recursive arm
-> the walk descends into the encoded declaring path, whose spine
declaration_reference_node builds at OccurrenceSynthetic
-> infer visited those spine nodes too, so each holds an entry with
grounding UNDERIVED rather than no entry, which is why the gate reports
grounding_not_derived and not a facts lookup miss.
The fixture's own positive control is enrolled beside it, so a later red is a
statement about eval and not about an assembly that stopped producing a call.
Both claims PASS on this base.
This corrects the earlier grouping. Three subjects sharing a reason string is
not evidence of one defect; a synthetic occurrence is a provenance category, and
two of those subjects contain applications of their own. They are grouped only
once their failing nodes and consumer paths agree, and this file establishes the
failing node for THIS subject alone.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… descending into
WHAT NOW EXECUTES. A call whose callee is a resolved corpus-declaration reference
dispatches through the declaration it names and returns that declaration's value.
Both executing controls assert the VALUE and not merely acceptance -- any
Int-returning path would satisfy "Accepted" while proving nothing about which
declaration ran, and 7 is written only in the callee's body.
THE CHAIN, one authority per link.
resolved declaration reference
-> canonical declaration identity (symbol_index_lookup, the GUARDED reader)
-> recorded on the reference's facts (InferredFacts denotation)
-> read by eval, which re-resolves nothing
-> the existing arrow dispatch: find_arrow_body_child, eval_bind_arrow_params
-> the callee's own body in the callee's own frame
Infer records the denotation because infer is the stage HOLDING the symbol index.
eval holds none, so the two routes otherwise open to it were both defects: a
second resolution path over the tree would be a WEAKER authority that accepts
references the ambiguity guard refuses (DESIGN section 3), and reading the body
out of the callable TYPE evidence would conflate two facts. The denotation is a
field separate from the grounding for exactly that reason -- a consumer wanting
the body reads the denotation, one wanting the type reads the grounding -- and
only a GROUNDED reference carries one, so a refused contract reaches no body.
WHY THE WALK WAS THE DEFECT BEFORE THE DISPATCH WAS. eval's callee classifier
admitted an Arrow and a bare Atom; a resolved reference is a marked Conj, so the
callee edge was not recognized, eval_fold_child_for_edge took its ordinary
recursive arm, and the walk descended INTO the reference's encoded declaring
path. The classifier now asks declaration_reference_path_optional -- the same
reader infer and translate ask -- rather than admitting Conj, which would admit
every record shape with it.
A REFERENCE REACHING NO EXECUTABLE DECLARATION REFUSES as an unbound runtime
binding and does not fall through to the primitive table, where it would be
looked up under a name it does not have and reported as a missing primitive
rather than as the declaration it names. The discriminating negative is enrolled:
a callee naming no declaration must not execute.
WHAT IS NOT DONE, enrolled executed and expected-red rather than described.
- PARAMETER BINDING IS NOT DEMONSTRATED. Both executing controls have CONSTANT
bodies, so a callee ignoring its argument entirely would pass both. The
parameter-bodied fixture -- whose value depends on the argument -- still
refuses. That claim is the one that would demonstrate binding and it is red.
- A BOOL-RETURNING CALL still refuses, and it is a DIFFERENT boundary: its body
is a constant, so it differs from the executing control only in return type.
TWO CORRECTIONS TO THE PRECEDING COMMIT'S READING.
The anchor measured there is an EMPTY Conj. An empty Conj is structurally equal
to any empty product, and node equality here is structural, so "inside the
declaring path" is weaker evidence than that commit's wording implies -- it is
consistent with the spine's nil terminator and does not exclude an unrelated
empty product. The classifier/walker mismatch stands on its own, established by
source and confirmed by the repair executing; the anchor comparison corroborates
it rather than proving it.
Four claims in v2.test.long.add_arrow_eval_by_execution fail on the pinned base
BEFORE this change (measured by stashing it), so they are pre-existing and not
caused here. I had no baseline for that set when I first read them as a
regression.
A CHANGE TRIED AND DROPPED. eval_fold_is_callee_reference_edge identifies the
callee edge by a processed-count, which is only correct while the callee is the
first child processed. That looked like the reason a one-argument call refused
where a zero-argument call executed, so it was rewritten to key on
eval_transform_callee_edge. Measured, it changed no verdict in either direction:
all seven controls pass without it. It is dropped rather than kept as an
unneeded second formulation, and the count-based identification is left as a
standing observation about that predicate, not a repair this change needs.
The carrier widening is five construction sites, not the forty-four a first grep
suggested: most matches were `-> InferredFacts {` signatures, and the fixtures
construct through helpers.
Regression: all 9 reference-evidence claims still pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…call WHAT THE REMAINING NAMED-CALL REFUSAL ACTUALLY IS. InferredTree keys its facts by Node; Node equality is structural over kind, children and occurrence identity; and std.occurrence_identity spells "no authored occurrence" as the NULLARY constructor OccurrenceSynthetic, so it is one VALUE and not one value per synthetic node. Two synthetic nodes with the same kind and children are therefore THE SAME KEY, whoever built them and whenever. Measured: the evaluator builds an empty synthetic Conj at runtime (v2.std.runtime runtime_value_conj_node, for a value's type), asks the facts map about it, and the map ANSWERS -- with the facts of an unrelated node that merely shares the shape. Those facts carry GroundingNotDerived, so eval refuses with eval_rejected_grounding_not_derived located at a node that exists in no source position. Three claims enroll it: the refusing node is equal to the runtime-built empty Conj; the map answers for that node; and a structurally equal node occurs in the program, which is what makes it a collision rather than a stray key. THE COLLISION IS SILENT IN BOTH DIRECTIONS, and only one direction is observed here. A lookup that should MISS instead hits, converting a fail-closed infer_facts_lookup_miss into a grounding judgment no producer intended. Had the colliding entry been DERIVED rather than underived, the same collision would hand the runtime a grounding nothing established -- a fabricated plausible output rather than a refusal (DESIGN section 5). Nothing currently makes that direction unreachable; this corpus just happens to collide with an underived entry. A CORRECTION I OWE, and it retracts my own evidence rather than someone else's. Commit b65297c attributed this refusal to the callee's encoded declaring path because the anchor was a member of that path's node set. That evidence does not discriminate: an empty synthetic Conj is a member of almost any node set it is tested against, including the spine's terminator, which is why the same probe also answered yes for the call subtree and for the declaration. The anchor comparison establishes nothing about location and should not have been read as attribution. What the classifier/walker repair rests on instead is unaffected: it is established by source -- the classifier admitted Arrow and Atom only while a resolved reference is a marked Conj -- and by named calls now EXECUTING to their callee's value, asserted by value and not by acceptance. That evidence does not pass through the anchor. WHY THIS STOPS HERE. The repair is to decide the KEYING RELATION for the facts map -- occurrence identity rather than structural identity -- which is a semantic rule about node identity, sits in the conformance-identity domain (DESIGN section 3b), and changes every facts lookup in the corpus rather than anything in this lane. Escalating rather than reaching for a local guard at the symptom link, which is the shape DESIGN section 6b names. The parameter-bodied and Bool-returning controls beside this file stay enrolled executed and expected-red; this finding explains the node they refuse at without yet discharging either. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The Bool-returning control's callee body is a constant, so it differs from an EXECUTING control only in its return type, and it refuses at the same runtime-built empty synthetic Conj as the parameter-bodied one. So this lane's two remaining reds have ONE cause rather than two. Scoped deliberately to these two subjects. A matching reason string is not evidence of a shared defect -- that was the error in an earlier grouping of three unrelated subjects -- so this claim compares the failing NODES and says nothing about any other refusal reporting the same reason. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…eration
I WAS TOLD MY EVIDENCE REPEATED THE ERROR IT CORRECTED, AND IT DID. The previous
commit replaced "the anchor lies inside the declaring path" with "the anchor is
what the runtime value constructor builds". Both were inferred from Node == Node,
and equality is the relation under suspicion, so it cannot be the instrument that
establishes provenance. An empty synthetic Conj compares equal to many unrelated
nodes; membership in a node set and equality with a constructor's result are both
uninformative about origin. Both readings are withdrawn.
WHAT ENUMERATION ESTABLISHES INSTEAD, which needs no provenance claim. Walking
infer's own entry list for one small program: MORE THAN ONE ENTRY carries the
empty synthetic Conj as its key, and those entries DISAGREE on whether grounding
was derived. So one key names at least two subjects whose facts differ, and a
consumer asking under that key receives whichever the first-match scan reaches
first. The same conflict stands in a second fixture, so it is a property of the
keying relation over ordinary programs rather than an artifact of one source text.
This is stronger than the earlier claims and differently shaped: it is not that a
freshly built equal value gets an answer, but that the relation ADMITS CONFLICTING
FACTS FOR ONE KEY. facts_map_from_entries checks each entry's own subject
correspondence and establishes no uniqueness or conflict condition across entries
that compare equal.
AND THE FAIL-OPEN DIRECTION IS REACHABLE, not hypothetical. A DERIVED entry exists
under the same key as an underived one, so a subject whose grounding was never
established can receive one that was -- a fabricated plausible output rather than a
refusal (DESIGN section 5) -- and which of the two a consumer gets is decided by
entry order. I had flagged this direction as a credible risk; the enumeration is
what makes it an observed reachability rather than a hypothetical, and it is still
short of an observed successful misexecution.
THE TRAVERSAL PATH, measured with a temporary diagnostic that gave each grounding
demand site in the evaluator its own reason symbol. The instrument is removed and
its result is recorded here rather than asserted, since asserting it would mean
keeping instrumentation in the evaluator:
- the demanding caller is eval_fold_init, through eval_fold_child_for_edge's
ORDINARY RECURSIVE ARM -- the node entered the walk as a child, not as a fold
root, so this is a traversal that descended into it rather than a consumer
asking about a supplied subject;
- the node sits under a NAMED edge and is NOT under the declaration-reference
marker, so it is not the reference spine the previous repair addressed;
- no node in the call subtree carries it as a POSITIONAL child, which is how the
named-edge conclusion was reached.
That locates the demand without asserting where the node came from, which is the
distinction the previous commits lost.
ALSO CORRECTED, and this one was a live defect rather than a wrong reading. The
annotation above eval_fold_is_callee_reference_edge described the callee-edge
identity repair as landed while the function still contained `p == 0 &&
is_positional(edge)`: I reverted the change after measuring that it moved no
verdict, and left the comment claiming it. A comment asserting a repair the
function does not contain is worse than no comment, since no Accepted program can
read one to check it (DESIGN section 4c). It now records the count-based
identification as a standing observation, states that rewriting it changed no
verdict in either direction, and says what would justify revisiting it: a call
shape where the two formulations DISAGREE, which is the discriminating case this
lane never found.
Verified after removing the instrumentation: all 7 declaration-reference eval
controls pass, including both executing calls; the 4 key-conflict claims pass. The
two executing controls return Accepted with diagnostics None, checked explicitly --
so they are executions and not acceptances carrying a suppressed refusal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ool pair THE NEXT RESULT IS NOW WRITTEN AND EXECUTED, not described. Three claims specify what "argument-dependent execution" means and run the comparison that decides it: identity(only_arg: 3) -> 3 identity(only_arg: 8) -> 8 TWO arguments, because one would not discriminate -- a callee returning a constant that happened to equal the argument would satisfy a single case. The callee's body IS its parameter, so its result cannot be produced without consuming the supplied argument, which is the gap the two constant-bodied executing controls leave open: a callee ignoring its argument entirely passes both of those. They are enrolled as the REFUSAL they are today, with the value path supplied and compared, so what remains when the boundary is repaired is inverting the assertion rather than authoring the behaviour it checks. Writing it the other way round would land a red and specify the same thing. ONE OF THEM IS VACUOUS TODAY AND SAYS SO. The claim that the identity callee must not answer the OTHER argument's value holds for the wrong reason while nothing executes -- both conjuncts are satisfied by refusal. It is enrolled anyway because it is the check that stops the repair being credited by a callee that consumes its argument and returns the wrong one, and it becomes discriminating the moment the claim above inverts. The annotation states the vacuity so no reader counts it as present coverage; an expecting-green claim that cannot currently fail is specification without execution unless its state is declared. THE BOOL PAIR GETS THE SAME TREATMENT one type further on: a true-returning and a false-returning callee must produce DIFFERENT answers, because a repair making both execute to the same value would satisfy "executes" while destroying the distinction the pair exists for. Every one of these refuses at the shared facts key rather than at anything about calls, arguments or return types -- the conflict is established by enumeration in v2.test.claim.callexec.synthetic_facts_key_collision, where more than one entry carries one key and those entries disagree on grounding. So this lane's acceptance result is blocked behind that one contract question and is fully specified while it waits, rather than waiting to be specified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…k that closes it
THE FRONTIER WAS DECLARED AND IT IS NOW PERFORMED. Two headers named this exact
gap. v2.compiler.body_lowering_fold PostfixAccum keeps `a.b.c` as ONE qualified
name and says why -- "deciding here would be a second resolver with no scope to
consult" -- naming try_resolve_qualified_name_node as the decider. That function's
own header then said: "Head bound and no absolute hit: the projection this arm
cannot yet perform, refused Unbound rather than fabricated." So the spine arriving
at resolve was never a producer defect; answering Unbound for it was resolve
accepting the job and not doing it, and the two causes -- a bound head needing
projection, and a genuinely unbound name -- were reported identically.
MEASURED FIRST, so a later green is a change in behaviour and not in the question.
On the pinned base, `fn f(b: Box) -> Int { b.tree }` refused at RESOLVE with
resolve_reason_unbound_symbol anchored on a QUALIFIED-NAME SPINE, while the same
receiver with the projection removed resolved and inferred. So the representation
was not reaching resolve as a projection at all.
THE THREE STAGES.
resolve a bound head with no absolute candidate becomes a field projection: the
head resolves to its binder through canonical_atom, and each remaining
segment folds on left to right, `b.x.y` as `(b.x).y`. It reads segment
NODES, not the name's symbols, so every field keeps the occurrence of its
own token and a diagnostic about one field lands on that field rather
than on the whole chain. The reader for that lives in
v2.std.qualified_name beside the spine's other reader and its inverse,
because that module owns the label set.
infer a projection is typed by the field the receiver's type declares. It sits
at the HEAD of the product row because a projection is an ELIMINATION,
not a record: without it the projection Conj is typed as the product of
its own children, a type combining the receiver with the field-name atom,
which is the type of nothing the program computes. The receiver's type
comes from its own facts through the row's entries; the type's fields come
through the same GUARDED index reader the callee path uses. This is the
first production consumer of v2.std.node_query declared_field_named.
eval a projection selects the field from the receiver's value. The receiver
arrives as the one runtime argument through the existing seam, so the base
is evaluated ONCE by the ordinary walk rather than re-entered per
projection. The field edge is deliberately not an argument: it carries a
name, not a value.
THE ABSENT-FIELD CONTROL EARNED ITS PLACE TWICE. With resolve's arm landed and
infer's absent, `b.absent_field` inferred CLEAN -- resolve admits the shape and
nothing checked the field, so a misspelled field became an accepted program. That is
the fail-open the control exists to catch and it caught it.
AND IT CAUGHT A SECOND ONE, IN MY OWN REPAIR. My first infer arm collapsed two
unavailabilities into one Absent: "I could not establish the receiver's type" and
"the receiver's type is established and declares no fields". That is the absorbing
fallback DESIGN section 5 forbids -- it converts a decided negative into "no
evidence" -- and it broke the standing negative control
v2.test.claim.namespace_xl0.cross_module_reference_resolution
a_receiver_with_no_such_child_never_accepts: `Bool.v` passed at the frontier. The
two are now separate arms. ReceiverTypeUnderived waits at the frontier, because
convicting a program whose receiver is typed by a route not yet reaching here would
be wrong in the other direction. ReceiverNotARecord REFUSES.
TWO CONTROLS IN ANOTHER LANE MOVED STAGE, AND THE PROPERTY IS STRICTLY HARDER NOW.
Both asserted refusal AT RESOLVE with resolve_reason_unbound_symbol for a `Bool`
receiver. Resolve no longer refuses those -- it commits the shape -- and infer
refuses them instead. So they now assert through infer: acceptance is still
forbidden, and the claim is harder than before, because a program that resolved and
then inferred clean would fail it where previously only the resolve reason was
checked. The old reason was the collapse rather than the property, which
v2.compiler.resolve's own header already recorded as a defect. One was renamed:
"refuses_unbound_today" pinned a stage and a reason it never meant to pin, and what
the row is FOR is that a method call on a local receiver is not silently admitted.
WHAT EVAL'S EVIDENCE IS AND WHY. Its receiver value is SUPPLIED, which is DESIGN
section 3's witness rule: the subject is one interface -- what eval returns for a
projection over a given aggregate -- and computing the aggregate would re-run
production the claim is not about. The pairing obligation is discharged by a claim
in the same file rather than by assertion: fps_the_resolved_tree_carries_a_field_-
projection asserts the real producer emits this shape over the production route.
A FINDING BEHIND THAT CHOICE, measured while looking for a fixture that would
deliver a projection to eval through surface syntax. Two forms that should, do not:
`Box { .. }.tree` and `make().tree` both resolve and infer with NO field-projection
node in the tree, while the parameter form `b.tree` now produces one. So the
value-receiver path body_lowering describes (PostfixAccumValue, the accumulator
after a call suffix) is not reached from these forms, and the only projection this
corpus's surface syntax currently produces has an unbound receiver at eval -- whose
binding is blocked behind the frozen facts-key question. That is why eval's executed
evidence is at its own boundary and not through a whole-program run.
A TYPE ERROR WORTH RECORDING, because it cost two iterations and will recur.
list_at_optional answers Optional<T>, and a value destructured straight out of it
does not carry its type through a FIELD ACCESS: reading `aggregate.fields` inline
produced a runtime type error while the sibling arm, which reads no field, passed.
Naming a typed parameter restores it. The same shape appears twice more in this
change, in the runtime field walk and in the spine segment reader.
Green: 13 field-projection controls (resolve, infer and eval, valid and absent
field, and two refusal arms) and 15/15 in the namespace lane.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…form
WHAT THE SEVEN'S REAL SITE ACTUALLY IS. In v2.test.parse.expression_bodied_fn_decl_-
parse the projection is `artifact.tree`, where `artifact` is bound by the arm
`Accepted { value: artifact, diagnostics: d }`. That is a MATCH-ARM BINDER, not the
function parameter the controls beside it use, so whether the projection repair
reaches it is its own fact and gets its own controls.
MEASURED: resolve reaches it, infer does not, AND THE ISOLATING CONTROL SAYS WHY.
The match form resolves -- resolve's projection arm handles a match binder's head
exactly as it handles a parameter's -- and then fails to infer. The same match form
with the projection REPLACED BY A LITERAL fails to infer identically. So the blocker
is the match construct, not the field access: it is the pre-existing match-arm
boundary already recorded as the seven's first refusal
(body_lowering_reason_match_arm_navigation_refused), owned elsewhere.
Both conjuncts of that claim are load-bearing. The projection form refusing alone
would be consistent with a projection defect; it is the literal-bodied form refusing
too that assigns the refusal to the match construct. When match arms do infer, the
claim goes red and the projection claim beside it becomes the live question, which is
the transition worth being told about.
A VACUOUS CLAIM OF MINE, CAUGHT AND REPLACED. I first asserted that an absent field
off a match binder is not admitted, and it PASSED -- vacuously, because the VALID
projection off a match binder does not infer either. Both arms refuse, so the
assertion distinguished nothing and would have gone on reading as coverage for the
absent-field wall on that shape. The isolating pair replaces it. This is the second
time in this lane that a claim passed while establishing nothing, and both times the
cause was the same: asserting a refusal without first checking that the positive case
reaches the boundary being tested.
AND THE SEVEN THEMSELVES ARE NOT THE EVIDENCE, DELIBERATELY. All seven pass under the
development runner -- both before and after this change -- because that runner
resolves them with the SEED compiler, while their blocker is v2's OWN front end on the
native route. Reporting that green as progress would be citing a signal that was never
about the property claimed, so the shape is reproduced as a small fixture instead and
the seven are left to the route that actually exercises v2.
Green: 15 field-projection controls.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
84 commits of main, and the conflict is the one this lane has been carrying: main threaded `kinds: List<RosterKindIndex>, tree: Node` through the same infer functions where #12432's carrier threads `resolved: ResolvedTree`. 33 conflicts in 04_infer.dag, 2 in 05_eval.dag, 1 in a type-param test. RESOLVED AS THE UNION, NOT A CHOICE. Every signature and call site keeps main's `kinds` thread AND the `resolved` carrier, with main's bare `tree: Node` dropped in favour of `resolved.root` -- which is what #12432 established the carrier for. Taking either side alone would have deleted a landed thread or reverted the carrier. Two conflicts were semantic rather than threading, and both take the union: - main added eval_callee_body_refusal_reason, a per-body-form refusal so a callee whose body is a function value refuses under its own reason instead of the generic unsupported-callee. Kept, and pointed at `callee_target` -- this lane's dispatch subject, the DENOTED declaration -- so the better reason is reported about the node the call actually dispatches through. - infer_established_return_type_optional is this lane's addition and main has no counterpart; kept with both its consultation sites. A MECHANICAL PASS THAT OVERREACHED, CAUGHT BY THE COMPILER. Rewriting `tree:` to `resolved:` across conflict hunks also hit two sites where `tree` is a genuine Node argument and not the carrier -- infer_transform_derived_optional's tree parameter and partial_bounded_lattice_instances_in_tree. Both now pass `resolved.root`. The fail-closed front end named all four errors by parameter, which is why a blind pass was survivable here; it is not a technique to repeat. NOTE FOR THE NEXT RUN: the seed's Rust moved substantially under these 84 commits (v1_interpreter.rs alone is +967 lines), so every claim_batch verdict taken with the pre-merge binary is stale and none is carried forward. The binary is rebuilt before any verdict in this lane is reported again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ce-consumer # Conflicts: # src/v2/compiler/00_compile.dag # src/v2/compiler/03_name_resolve.dag # src/v2/compiler/03_resolve.dag # src/v2/compiler/04_infer.dag # src/v2/extdeps/languages/dag.dag
…oduced Reverts 6b3490b. That commit replaced `dag_canonical_symbol_map`'s route to the carried symbol set -- reading the grammar's fields directly instead of building a whole `Node` encoding and sweeping it for atoms -- and proved EXACT SET EQUALITY against the old derivation as its central evidence. The equality proof is what makes it wrong to keep. main has since NARROWED that set deliberately, and its reasoning names a silent-wrongness class: carrying the grammar's atoms "made an unbound `node` in a body resolve, Accepted and silent, to a grammar atom, and a declaration spelled `output` resolve to the kernel symbol rather than to its path". main's set is now the lex token classes plus the kernel bindings -- what the model mints as atoms a resolved body may carry -- and NOT production names or contextual-keyword terminals, which parse consumes in their grammar positions and which never reach resolution as references. So the reverted commit is a faithful, measured, well-controlled reproduction of a defect. Its equality control established that the new route reproduced the old set exactly, which is precisely the property main removed. Resolving the merge toward it would have reverted a correctness fix for a class DESIGN §5 forbids outright -- a wrong answer passing silently -- in exchange for a demand-minimization win already measured at roughly 0.1 s of a 201.8 s native context, since `dag_language_model` is prepared once per run. NOTHING IS REBASED ONTO THE NARROWER SET, because against it there is likely nothing left to minimize: main's derivation is token classes plus kernel bindings and does not go through `grammar_to_node` at all. Keeping `grammar_carried_symbol_map`'s rewritten form and its equality control would leave an authority for a set nothing consumes, which is the dangling modeling DESIGN §3c forbids. `grammar_carried_symbol_map` returns to its serialized-image form, which main carries independently of this lane and which `grammar_carries_symbol` still consumes, so the revert removes only what this lane added. WHAT THE REVERT DOES NOT DISCARD is the reading that motivated it: a route that builds a representation nothing consumes, purely so a walker can read back facts its source already names, is authored duplication. That remains true of the old route and is recorded here rather than in a live declaration, because the subject it applied to no longer exists. The three canonical_demand claim files go with it, including the consumer control whose citation was sharpened in a509caa: it exercised the wide set's membership through resolve, so it asserts a property main has deliberately removed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r loss at its refusal
Integration repair for the main merge. Two rows in
v2.test.claim.field_projection.field_projection_stages went red against main's
change to how a named fn's parameter grounds, and they needed opposite treatments
because only one of them was still asserting something achievable.
REPAIRED: THE PARAMETER COMPARISON'S READER, NOT ITS ASSERTION.
`fps_body_atom_type_optional` searched the inferred tree for a bare
`Atom { identity: ^i }`. main now mints a named fn's parameter as a path-keyed
PARAMETER REFERENCE grounded through the resolved declarations, so that search
found nothing and `fps_int_parameter_type_optional` answered Absent. A probe
separated the halves: the field's own grounding was still present and only the
parameter side had gone, so the row failed on its COMPARISON BASIS rather than on
its subject. The reader now asks `parameter_reference_path_optional` and matches
the declaring path's leaf through a new `fps_path_leaf_is`. What the row
establishes is unchanged -- two independent inference routes agree on one type --
which is why the reader moved and the assertion did not. Weakening it to compare
against a directly constructed `Int` node would have made the control share its
derivation with its subject.
RECORDED AT THE REFUSAL: THE MATCH-ARM BINDER AS A RECEIVER.
That capability is gunbc#12641's, it is LANE-ONLY and never reached main, and main
froze `infer_parameter_scope_search` to LAMBDA parameters. A match-arm binder is
neither a lambda parameter nor a path-keyed reference, so it falls between the two
routes: the fixture resolves and then stops with `infer_grounding_not_derived` and
no more specific cause. `fps_a_match_binder_receiver_does_not_yet_infer` now
asserts that refusal, and `fps_a_match_binder_projection_is_in_the_resolved_tree`
reads the RESOLVED root rather than the inferred one -- reading the inferred tree
would be vacuous, there being no inferred tree to read, and the row exists to keep
the refusal row from being satisfied by an absent subject. Neither row claims a
wall; an absent field off a match binder is not refused either, which is the
ordinary consequence of an underived receiver and not a fail-open. The restoration
trigger is stated as a capability, and under DESIGN §4b(4) both rows become the
controls that the restoration stays real rather than retiring. A §4b(3) rung-drop
row on #12641's subject may also be owed; it is flagged in the header rather than
filed, because that capability belongs to that change and not to this lane.
THE CAUSE WAS ATTRIBUTED BY PROBE, NOT BY ARGUMENT, which matters because three
of this lane's own changes were the obvious suspects. Each was bypassed in turn and
the rows failed identically every time: the value-binder gate, the closure
resolved-declaration index (restored to `resolved_declarations_of`), and the
match-arm walk, whose admitted body is byte-equivalent to main's inlined version
with only the gate wrapped around it. The `ArmBinder` route survived the merge
intact -- nine of ten occurrences, the single loss being a COMMENT line -- and the
search's entry points and `resolve_pattern_binders` are byte-identical to their
pre-merge forms. So the lane's code is present and its inputs moved.
ALSO IN THIS COMMIT, all consequences of the same merge:
`infer_type_decl_formation_facts_from_entries` threads the `resolved` this lane
added to the product row beneath it, which main's caller could not have passed.
`resolved_declarations_over` passes main's new `resource_declarations`, and the
inherited-roster note now covers resources as well as records.
`resolve_match_arm_admitted` carries main's `kind: LexicalFrame` and is called by
the gate rather than duplicated inside it. `native_test_closure_resolved_roots` is
DELETED: main's refactor moved index, active_roots and policy into the resolution
context, so `closure_resolved_roots` takes two arguments and the wrapper became a
thin alias -- the call is inlined instead. Two helpers the rewrite left with no
callers (`fps_match_binder_projection_grounds`, `fps_match_no_projection_source`)
are removed as §3c dangling, and a kept discriminator is renamed from its probe
name to `fps_a_multi_root_ingest_does_not_itself_break_retrieval`.
RECEIPTS: field_projection_stages 24/24, declaration_reference_evidence 11/0,
cross_module_reference_resolution 15/0, projection_dispatch.receiver_disposition
2/0 -- 52/52 -- and `00_compile` compiles with 0 blocking errors. The claim files
alone did not establish that last one: at the point every claim set was green,
00_compile still carried 5 blocking errors, all of them in the wrapper this commit
deletes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ce-consumer # Conflicts: # src/v2/compiler/body_lowering_fold.dag
main changed all three inlined arrow builders to wrap in `close_lowered_image` while this lane had replaced those three copies with one `body_lower_callable_arrow`. The helper now applies it, so every caller gets main's behaviour from one place rather than from three, and main's `declared_signature(params: [], source: shell)` correction -- a real change carried inside the same restructuring hunk -- is taken rather than lost to the structural difference. That is the second time in this merge that main's side held a small correction inside a large restructuring, so taking "our" side on the structure would have silently reverted it. One call site kept main's second closing paren, which `close_lowered_image(node_lowered_from(` needs and the helper does not. It surfaced from the closure loader as `reference_closure: has no readable reference set (cause=parse-failed)` rather than as a located syntax error, so the site had to be bisected -- worth knowing that a parse break in a FOLLOWED module reports as an unreadable reference set and not as a syntax error with a line. RECEIPTS at this head: `00_compile` 0 blocking errors / 221 files emitted; field_projection_stages 24/0, declaration_reference_evidence 11/0, cross_module_reference_resolution 15/0, projection_dispatch.receiver_disposition 2/0, fold_lowering 20/0 -- 72/72. fold_lowering is included because this merge touched body lowering, and the claim files that were green before it would not have caught a regression there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the matrix chose The required floor refused with four causes, all in modules this lane's claim matrix never compiles. One is this lane's own omission and three are the merge's consequences in test modules main moved under. MINE: v2.compiler.self_host.closure_emission is a THIRD caller of resolved_tree_outcome. Widening that constructor, I fixed the two call sites I knew about and never enumerated the rest. It resolves one member module and holds no closure, so an empty closure_roots is both correct and behaviour-preserving -- which is exactly what the helper's header says an empty list means, so the fix was never hard; finding the site was the whole problem. MAIN'S, IN LANE TEST MODULES: a ScopeFrame literal gains main's new kind field (LexicalFrame); a ResolveContext literal gains main's new declaring field, set to NotDeclaring, because a supplied context for a binder-admission slice declares nothing and a path there would be a fabricated fact; and declaration_reference_spine_optional is now the kind-parameterised resolved_reference_spine_optional, asked with DeclarationReferenceKind. THE PROCESS FAILURE IS THE POINT. A standing note says to compile every consumer closure after widening a signature, and the floor's population is the corpus while mine was five files I picked. 72/72 green claim rows plus a clean 00_compile is not evidence about closure_emission or these two test modules, because none of them is in those closures. The number was real and the population was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The emitted crate failed to typecheck: closure_resolved_roots wants the
Outcome<ResolutionContext> that a NativeTestContext HOLDS, and this call site handed
it the context itself.
expected Rc<Outcome<Rc<ResolutionContext>>>, found Rc<NativeTestContext>
The field is step.context.resolution, which is what the sibling reader
native_test_resolve_module_walk already passes.
WHY THE FRONT END DID NOT CATCH IT, which is the part worth keeping. `gunbc compile
--dry-run` reports 0 blocking errors on this same source. The two types only become
distinct after lowering to Rust, where each becomes its own Rc<...>, so for this lane
a clean .dag front end is NOT evidence that the emitted Rust compiles. The required
emit-build lane is what establishes that, and the gap between them is exactly the
one that let a wrong readiness claim stand: claim rows and 00_compile were green while
the emitted crate did not build.
RECEIPT: emitted to a kept directory and built directly --
225 files emitted, then `cargo build --release` with RUSTFLAGS="-D warnings" finishes
clean. Reproducing it that way rather than through the instrument is what made the
error readable: the instrument reports EmittedCompilerBuildFailed with
diagnostic=unattributed and a truncated stderr_tail, and its probe root is removed
before it can be inspected.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The floor's declarations phase refused with CITED-DECLARATION-ABSENT: gunbc.generic_binder_field_projection_deficit cites v2.test.claim.fold_lowering lowered_loop_binds_carrier_binder, which that module no longer declares. Earlier in this lane that row was renamed to lowered_loop_carrier_is_a_generated_slot_not_the_authored_binder, when the fold carrier became a generated slot rather than the authored step formal, and the citing sites were not updated with it. THERE WERE TWO, AND THE FLOOR NAMED ONE. The second is a membership string inside v2.workflow.floor_cost_debt's roster, which the declarations check does not reach, so a grep for the old name is what found it. That is the §3 argument for citing a symbol rather than a position doing its job in reverse: the rename was decidable from the name, and both sites were mechanically findable once one of them refused. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ot the collision All three rows in v2.test.claim.callexec.synthetic_facts_key_collision asserted `total > 1` -- that more than one inferred-facts entry stood under a single key, because structurally identical synthetic nodes keyed one entry and eval could refuse at a node that was not its subject. gunbc#12582's facts-key work eliminated that, so all three failed. MEASURED BEFORE FLIPPING: exactly ONE entry stands under the key, for both fixtures. That matters for how the rows are written -- `== 1` rather than `<= 1`, because a fixture that stopped producing the node at all would answer 0, and a `<= 1` row would sit green while testing nothing. The count is enumerated rather than inferred from a lookup, which the original rows did for the same reason: a lookup answering something proves only that SOME entry matched, while counting proves how many stand there. DESIGN §4b(4) IS WHY THEY FLIPPED RATHER THAN RETIRED. A climb deletes the lower-rung production handling and keeps the evidence, so each row keeps its fixture and its counting method and now asserts the separation: exactly one entry under the key, that entry grounded, and the same separation reached by a second fixture -- which is what the original third row established in the opposite direction, that the property belongs to the keying relation over ordinary programs rather than to one source text. They go red the moment two entries share a key again. 4/4. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…d lookup INCOMPLETE ON PURPOSE, and the title says so because the next reader must not take this for a working repair. It introduces the keying gunbc#12766 declared as a frontier owned by this lane's named-call route, and that keying cannot take effect until a separate gate is opened. WHAT IS HERE. `eval_parameter_binding_key` derives an EnvironmentBindingKey from a full parameter path and is the ONLY place either side derives one, so binding and lookup cannot disagree -- which is the whole point, since binding by bare label while the body looks the parameter up by its declaring path is the two-authorities defect the frontier existed to prevent. `eval_formal_binding_key` decides which keying a formal gets: a callee that is a resolved declaration reference supplies a path and its formals key by path; a LAMBDA supplies none and keeps the lexical bare-label route #12766 deliberately left it on. A named declaration gets NO bare-label fallback, because binding both spellings would make the route look repaired while preserving both authorities. The callee's path is read off the reference the call already carries, so eval stays a consumer of resolution's answer and never becomes a second naming authority. The full path is keyed, never the leaf, so `p.f.x` and `p.g.x` cannot alias. WHY IT IS NOT EFFECTIVE, measured. The three argument-dependent cref controls still refuse, and NOT because of this keying: `v2.std.node` `arrow_body_admits_eval_entry` returns false for `ParameterReferenceBody` (v2.std.node:1101), and `eval_callee_body_refusal_reason` maps that same arm to ^eval_rejected_parameter_reference_unbound (05_eval:1791). So the reason has TWO PRODUCERS and the one firing is the pre-binding entry gate, located at callee_target, before eval_bind_arrow_params runs at all. A parameter-bodied callee never reaches binding; a constant-bodied one does, which is why four probes showed the named branch taken, non-empty ApplicationBound slots, and successful binds while the failing fixture was unaffected by any of them. THE REMAINING STEP, so it is not re-derived: admit ParameterReferenceBody through the canonical arrow_body_admits_eval_entry policy rather than with an eval-local exception, which would be a second authority for which body forms may enter eval. Then this keying is on the path and the lookup here answers. A genuinely unbound or wrong-path reference must still refuse with the same reason -- what disappears is the categorical refusal based only on the body's FORM. AND A WARNING FOR WHOEVER CONTINUES: do not infer a key mismatch from that reason. I did, and spent four probes on it. The first action is one claim comparing the fatal locus against the exact callee_target and body nodes; the source predicts callee_target. Nothing regresses: v2.compiler.eval resolves clean and the cref matrix is unchanged at 7 PASS / 3 FAIL, the same three rows and the same reason as before this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…and resolves by path The three argument-dependent controls in v2.test.claim.callexec.declaration_reference_eval now pass. gunbc#12766 made a named fn's parameter use a path-keyed reference and declared eval's keying a frontier whose trigger is this lane's named-call route; this closes it. 12/12. TWO DECISIONS WERE COLLAPSED INTO ONE REASON, which is why this took so long to see. ^eval_rejected_parameter_reference_unbound is raised BOTH by eval_callee_body_refusal_reason for the ParameterReferenceBody ARM -- before any parameter is bound -- and at a genuine lookup miss. I read it as a key mismatch and spent four probes on lookups by full path and by leaf and on binding under both spellings, none of which could touch the failing fixture: a parameter-bodied callee never reached binding, while the constant-bodied controls beside it did, which is exactly why those probes showed the named branch taken, non-empty ApplicationBound slots and successful binds. Twenty-one reason symbols were tested before I stopped guessing and measured the LOCUS instead, which answered on the first try. THE REPAIR IS TWO ARMS AND ONE KEY. v2.std.node arrow_body_admits_eval_entry admits ParameterReferenceBody. That is the canonical policy for which body forms may enter eval, so the change is made THERE and not as an eval-local exception, which would be a second authority for one decision. Admitting the form is not admitting the access: a missing binding still refuses. eval_runtime_node resolves a parameter reference as a LEAF. Its carrier is a marked Conj whose child is the encoded declaring path, so letting the data-flow fold see it descends into that path and demands value-grounding for the internal representation of a parameter identity -- the same defect this module already fixed for DECLARATION references at eval_fold_is_callee_reference_edge. Finding that the fold was the remaining link came from reading the dispatch after the gate opened, not from another probe. eval_parameter_binding_key remains the ONLY place either side derives a key: the bind side snocs the formal's label onto the callee's declaring path, the use side already carries that path, and both ask the same constructor. Full path, never the leaf, so p.f.x and p.g.x cannot alias. Lambdas keep their lexical bare-label route, which #12766 deliberately left them on, and a named declaration gets no bare-label fallback -- binding both spellings would make the route look repaired while preserving both authorities. EVIDENCE, INCLUDING THE FLIPPED MEASUREMENT. The locus row that identified the gate asserted the refusal was located at the callee's declaring Arrow; that refusal no longer happens, so under DESIGN section 4b(4) the row does not retire -- it now asserts the policy arm directly and goes red if it is reverted. Beside it, a supplied parameter reference whose path nothing bound still refuses with the same reason, which is what keeps admitting the form from being a widening and pins what that symbol now means: a missing binding and nothing else. NO REGRESSIONS: arrow_body_form_witness 33/0 (the policy's own witness), declaration_reference_eval 12/0, synthetic_facts_key_collision 4/0, field_projection_stages 24/0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Fifteen conflicts in five files, each resolved on its merits: - resolved_tree_of keeps BOTH widenings: closure_roots (this lane) feeds resolved_declarations_over, and lexical (main #12947) fills lexical_bindings. 00_compile and resolved_tree_outcome pass both. - arrow_body_admits_eval_entry admits ParameterReferenceBody (this lane) and LexicalReferenceBody (main). - 05_eval: main's lexical-reference route (bare-label key, matching lambda formals' eval_formal_binding_key Absent arm) coexists with this lane's path-keyed parameter leaf; main did not supersede the parameter path. eval_node_is_callee_reference recognizes declaration AND lexical references. - 03_resolve: this lane's value-binder admission gate stays a pure refusal in front of each site; the frames it guards are main's FrameBinders/lexical_frame (match arm, let). The loop-carrier comment keeps main's text plus this lane's dissolution paragraph. direct_atom_binding_fold is deleted as main did (no caller remains). - 04_infer: main deleted infer_parameter_scope_search (lambda parameters now read resolve's recorded binding). Taken. This retires the lane-only #12641 match-arm binder typing that rode on that walk (infer_binding_type_in_scope, infer_arm_pattern_binder_field) -- arm binders now arrive as lexical references with no declared type, so they are underived, the same loss this lane already recorded at fps_a_match_binder_receiver_does_not_yet_infer. Consumers the widened carriers broke outside the conflict set were updated (03_name_resolve, callable_binder_slice_test, match_binder_typing_test, field_projection_stages_test import, one ledger citation). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Three consequences of composing this lane with main's #12947 that git reported clean: - resolve_projection_base: a ParameterFrame-bound head now mints the path-keyed parameter reference through resolve_frame_bound_reference, as any other use of that parameter does. As a bare atom it was typed only by infer's scope search, which main deleted, so every projection off a named fn's parameter went underived (field_projection_stages 6 reds, back to 24/24). Lexical and type-parameter heads keep the canonical atom; carrying lexical entries through this Outcome<Node> route is a declared frontier with a capability trigger. - parameter_reference_test: main's shared program bound `let x` over parameter `x`, which this lane's value-shadowing ruling refuses, so the whole program refused and seven rows went red together. h's let now binds `z` (L1 reads it), and row (2) becomes the refusal on its own source, asserted by reason. - callable_binder_slice_test: main deleted add_arrow_domain_named_params (arrow_domain_frame_binders replaces it), and row (9)'s frame now records its binding and keys its use by a minted occurrence, as resolve's own frames do (9/9). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…counted Main's #12381 lowers `type Pos = Int where positive` to a zero-argument call of positive(x: Int) whose subject is implicit. This lane judges every named call (main judged none), so every refinement refused application_positional_deficit. #12381 carries no typed subject slot (the first-formal convention is an annotation in std.types, and brand takes no subject), so judging with the carrier needs new modelling, dispatched separately on main (calm-boar-904 ruling). Until then the predicate set is walked under the SAME declared frontier RefinementDeclaration.where_clause already carries, not a second row: infer_where_predicate_set_edge merges past the captured predicate set, and each predicate call emits inhabitance_undecidable_where_predicate_subject_ unmodelled at its own locus, so the population is counted by execution. Not a rung drop: predicate calls were unjudged before; every other named call stays judged, held by pr_ordinary_named_call_deficit_still_refuses. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…r parse refusal) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…212) closure_resolved_roots re-resolved every closure root for every subject a lane resolved, and resolved_tree_of then re-folded those roots into an index per subject: N x (N + 1) resolves and a second quadratic fill. The shared ResolutionContext is the least common ancestor of those demands (DESIGN 2), so the closure's resolved-declaration index is now produced on first demand by closure_declarations_demand and memoized on the context (closure_declarations), like the namespace provider beside it; the per-root resolves thread the context so the namespaces they admit are kept too. resolved_tree_of takes that index and fills only the subject over it. resolve_in_context and the native lane's native_module_resolve_verdict both return the memoized context, so the next subject reads it. field_projection_stages 24/24, declaration_reference_evidence 11/11, parameter_reference 14/14. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…at is not a sweep Main's typed non-fold-residue census (#12980) refuses a top-level wildcard over a closed coproduct without a row. Fifteen of this lane's sites matched NodeKind (two variants), so their wildcard is now the two explicit variant arms -- construction rather than a roster row; infer_coproduct_arm_pattern's multi-line remainder moved into infer_coproduct_arm_pattern_constructed so both arms call it. eval_field_projection_of_receiver matches RuntimeValue, where RuntimeAggregate is the only field-bearing variant and every other refuses identically, so it is rostered with its reason and dissolution. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… lane/reference-evidence-consumer Eight conflict hunks in five files, each resolved by keeping this lane's structure and taking main's label constructors inside it: the import unions in resolve/infer/eval, body_lower_callable_arrow and its callers (whose arrow-body edge is now core_edge_label(ArrowBodyEdge)), the fold seam's slot binder under main's LoopCarrierEdge etc., and resolve_match_arm_admitted reading the pattern edge through edge_is_core(MatchArmPatternEdge) as main's inline arm did. #12799 also broke lane code git merged cleanly, swept by grep for every lane-added Named label and every lane-added lookup of a symbol that became a core marker: infer's match-arm reads use find_core_child(MatchArmPatternEdge / MatchArmBodyEdge); variant-tag and pattern-field readers match Authored and give StructuralLabel its own arm (skipped for tags; refused as an unread pattern for fields); infer_where_predicate_set_edge matches Authored with a StructuralLabel arm; three test fixtures build Authored / core labels. No lane-added label match lacks the structural arm, and no lane-added code looks up a core symbol by name. Rebuilt claim_executor, gunbc and claim_batch for this tree (private CARGO_TARGET_DIR): parameter_reference 14/14, callable_binder_slice 9/9, field_projection_stages 24/24. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…the binder-typing drop Per calm-boar-904's ruling of 2026-10-02: FSR: v2.test.claim.projection_dispatch.fold_step_receiver is deleted. Its five fsr_dbg_* rows were mutually exclusive reason guesses, debugging scaffolding that could never all pass; the module never passed on this lane, and its fixtures die at an unrelated resolve_reason_unbound_symbol. Nothing imports it. Its fixture sources went to silent-crab-339 (N7-1), whose own controls replace it. MBT: of the six red rows, three were not the capability loss at all, and two reader defects explain them (all six were red at 2eb0676 too): - infer_match_variant_payload read a coproduct's variant edges through declared_field_from_edge, which answers only for a binder-node target since fields became binder nodes, so every tag read as undeclared and every match refused infer_match_pattern_variant_not_declared. A variant's payload is the target of its tag edge, and the payload's fields keep the field reader. The supplied fixture's declared fields are now binder nodes, as lowering writes them (mbt_field). mbt_a_field_the_variant_does_not_declare_refuses, mbt_a_missing_variant_refuses_as_non_exhaustive and the positive control mbt_the_supplied_match_is_accepted_and_typed pass again. - infer_field_pattern_binds read only a bare atom, but resolve walks a pattern field as an ordinary node and the arm frame answers the binder's own name, so the binder arrives as a lexical reference; it is now read by its label. The source route then infers instead of refusing infer_match_pattern_unread. The other three ARE the loss. Each now asserts today's state on its exact route -- the binder's use in `artifact.tree` underived, and infer_match_arm_body_type_underived reported at that projection's own locus (mbp_reports_at) -- so an unrelated refusal reds it, and it flips back when typing returns. That lowers #12641's landed capability, so it is filed as gunbc.rung_drop match_arm_binder_typing_lost_to_lexical_carrier (previous StructurallyGuaranteed, temporary Mitigatable, deleted without replacement when #12766 restricted the scope search to lambdas and main's lexical cut deleted it; trigger: match-arm binder typing through the lexical-binding carrier, N7-3), rostered in gunbc.rung_drop.roster. match_binder_typing 13/13. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ere-clause frontier The floor on 82187ba refused one row: fps_a_match_binder_receiver_does_ not_yet_infer asserted that the match-binder fixture REFUSES with infer_grounding_not_derived. That refusal was the pattern-field reader defect repaired in the previous commit; the program now infers and the projection off the binder is accepted underived, which is the rung drop's real state. The row is renamed fps_a_match_binder_receiver_is_not_yet_typed and asserts that state on its exact route (infers; the projection node found in the inferred tree; its facts carry no derived grounding), and the rung drop's population is updated to the new identity. field_projection_stages 24/24. The where-clause frontier stays PARKED (operator ruling via calm-boar-904, 2026-10-02): refinements are being deleted in favour of checked constructors returning Optional, so its trigger now names that removal, not a subject-slot model. Only the trigger text changed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ows WARM The floor on d9bcf94 passed every witness and then refused 55 new-witness identities as enrolment_measured_over_margin (72.3k-step budget). Five are this change's own: parameter_reference's let-shadowing and named-call-deficit rows each ran a front end (and one an infer) inline, and expression_bodied_ continuation's three normalize rows each ran a prepared parse plus normalize. Each is now one nullary producer answering the decided value (a reason Symbol; a Bool), listed in floor_cross_claim_pure_producers_warm with module-prefixed names, and the rows read it. Nothing moves to a long home or cost-debt. The other fifty (fps, mbt, dre, cref, sfk) are being restructured the same way by two helpers stacked on this head, per calm-boar-904's ruling. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
#12506's floor refused 25 identities in these three modules as enrolment_measured_over_margin: each row re-ran assemble -> resolve -> infer (-> eval for cref) inline, several fixtures twice. Each fixture is now one nullary producer answering a portable record of decided values (DreReading, CrefReading, SfkCounts); rows read it. Nothing is supplied, so every row still executes the real path and keeps its red; no assertion changes. claim_batch: dre 11/11, cref 12/12, sfk 4/4 PASS. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md match_arm_binder_typing_lost_to_lexical_carrier Heal-Candidate-Run: 37075795569
…' into session/bright-ant-369
briansrls
marked this pull request as ready for review
October 3, 2026 01:45
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fcce450379
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| Accepted { value: module_qn, diagnostics: _ } => | ||
| let walked = resolve_walk_in_context( | ||
| context: Accepted { value: acc.context, diagnostics: None }, | ||
| admission: Admission { subject: ResolutionSubject { name: module_qn }, imports: [] } |
There was a problem hiding this comment.
When a non-subject root uses any imported name, resolving it with imports: [] either makes that root refuse and disappear from the closure declaration index, or stores an empty-import namespace that later causes resolve_reason_namespace_provider_admission_conflict when the same threaded context resolves the module with its real admission. Consequently, valid declarations from providers that depend on imports remain unavailable to inference, and subsequent multi-module resolutions can fail solely because the closure scan poisoned the namespace cache; derive each root's actual admission or avoid committing these synthetic admissions to the shared context.
Useful? React with 👍 / 👎.
Contributor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
bright-ant-369.Pushing to
session/bright-ant-369advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan